Left Termination proof of /tmp/tmpHg2Z8K/pl7.6.2c.pl

Left Termination of the query pattern reach_in_4(g, g, g, g) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

reach(X, Y, E, L) :- member(.(X, .(Y, [])), E).
reach(X, Z, E, L) :- ','(member1(.(X, .(Y, [])), E), ','(member(Y, L), ','(delete(Y, L, V1), reach(Y, Z, E, V1)))).
member(H, .(H, L)).
member(X, .(H, L)) :- member(X, L).
member1(H, .(H, L)).
member1(X, .(H, L)) :- member1(X, L).
delete(X, .(X, Y), Y).
delete(X, .(H, T1), .(H, T2)) :- delete(X, T1, T2).

Queries:

reach(g,g,g,g).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in(X, Z, E, L) → U2(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U2(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3(X, Z, E, L, Y, member_in(Y, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U3(X, Z, E, L, Y, member_out(Y, L)) → U4(X, Z, E, L, Y, delete_in(Y, L, V1))
delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5(X, Z, E, L, reach_in(Y, Z, E, V1))
reach_in(X, Y, E, L) → U1(X, Y, E, L, member_in(.(X, .(Y, [])), E))
U1(X, Y, E, L, member_out(.(X, .(Y, [])), E)) → reach_out(X, Y, E, L)
U5(X, Z, E, L, reach_out(Y, Z, E, V1)) → reach_out(X, Z, E, L)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in(X, Z, E, L) → U2(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U2(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3(X, Z, E, L, Y, member_in(Y, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U3(X, Z, E, L, Y, member_out(Y, L)) → U4(X, Z, E, L, Y, delete_in(Y, L, V1))
delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5(X, Z, E, L, reach_in(Y, Z, E, V1))
reach_in(X, Y, E, L) → U1(X, Y, E, L, member_in(.(X, .(Y, [])), E))
U1(X, Y, E, L, member_out(.(X, .(Y, [])), E)) → reach_out(X, Y, E, L)
U5(X, Z, E, L, reach_out(Y, Z, E, V1)) → reach_out(X, Z, E, L)

REACH_IN(X, Z, E, L) → U2¹(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
REACH_IN(X, Z, E, L) → MEMBER1_IN(.(X, .(Y, [])), E)
MEMBER1_IN(X, .(H, L)) → U7¹(X, H, L, member1_in(X, L))
MEMBER1_IN(X, .(H, L)) → MEMBER1_IN(X, L)
U2¹(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3¹(X, Z, E, L, Y, member_in(Y, L))
U2¹(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → MEMBER_IN(Y, L)
MEMBER_IN(X, .(H, L)) → U6¹(X, H, L, member_in(X, L))
MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)
U3¹(X, Z, E, L, Y, member_out(Y, L)) → U4¹(X, Z, E, L, Y, delete_in(Y, L, V1))
U3¹(X, Z, E, L, Y, member_out(Y, L)) → DELETE_IN(Y, L, V1)
DELETE_IN(X, .(H, T1), .(H, T2)) → U8¹(X, H, T1, T2, delete_in(X, T1, T2))
DELETE_IN(X, .(H, T1), .(H, T2)) → DELETE_IN(X, T1, T2)
U4¹(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5¹(X, Z, E, L, reach_in(Y, Z, E, V1))
U4¹(X, Z, E, L, Y, delete_out(Y, L, V1)) → REACH_IN(Y, Z, E, V1)
REACH_IN(X, Y, E, L) → U1¹(X, Y, E, L, member_in(.(X, .(Y, [])), E))
REACH_IN(X, Y, E, L) → MEMBER_IN(.(X, .(Y, [])), E)

The TRS R consists of the following rules:

reach_in(X, Z, E, L) → U2(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U2(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3(X, Z, E, L, Y, member_in(Y, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U3(X, Z, E, L, Y, member_out(Y, L)) → U4(X, Z, E, L, Y, delete_in(Y, L, V1))
delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5(X, Z, E, L, reach_in(Y, Z, E, V1))
reach_in(X, Y, E, L) → U1(X, Y, E, L, member_in(.(X, .(Y, [])), E))
U1(X, Y, E, L, member_out(.(X, .(Y, [])), E)) → reach_out(X, Y, E, L)
U5(X, Z, E, L, reach_out(Y, Z, E, V1)) → reach_out(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4) = reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5) = U2(x2, x3, x4, x5)
member1_in(x1, x2) = member1_in(x2)
.(x1, x2) = .(x1, x2)
[] = []
U7(x1, x2, x3, x4) = U7(x4)
member1_out(x1, x2) = member1_out(x1)
U3(x1, x2, x3, x4, x5, x6) = U3(x2, x3, x4, x5, x6)
member_in(x1, x2) = member_in(x1, x2)
U6(x1, x2, x3, x4) = U6(x4)
member_out(x1, x2) = member_out
U4(x1, x2, x3, x4, x5, x6) = U4(x2, x3, x5, x6)
delete_in(x1, x2, x3) = delete_in(x1, x2)
U8(x1, x2, x3, x4, x5) = U8(x2, x5)
delete_out(x1, x2, x3) = delete_out(x3)
U5(x1, x2, x3, x4, x5) = U5(x5)
U1(x1, x2, x3, x4, x5) = U1(x5)
reach_out(x1, x2, x3, x4) = reach_out
DELETE_IN(x1, x2, x3) = DELETE_IN(x1, x2)
U5¹(x1, x2, x3, x4, x5) = U5¹(x5)
REACH_IN(x1, x2, x3, x4) = REACH_IN(x1, x2, x3, x4)
MEMBER1_IN(x1, x2) = MEMBER1_IN(x2)
U4¹(x1, x2, x3, x4, x5, x6) = U4¹(x2, x3, x5, x6)
MEMBER_IN(x1, x2) = MEMBER_IN(x1, x2)
U8¹(x1, x2, x3, x4, x5) = U8¹(x2, x5)
U2¹(x1, x2, x3, x4, x5) = U2¹(x2, x3, x4, x5)
U1¹(x1, x2, x3, x4, x5) = U1¹(x5)
U6¹(x1, x2, x3, x4) = U6¹(x4)
U7¹(x1, x2, x3, x4) = U7¹(x4)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x2, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

REACH_IN(X, Z, E, L) → U2¹(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
REACH_IN(X, Z, E, L) → MEMBER1_IN(.(X, .(Y, [])), E)
MEMBER1_IN(X, .(H, L)) → U7¹(X, H, L, member1_in(X, L))
MEMBER1_IN(X, .(H, L)) → MEMBER1_IN(X, L)
U2¹(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3¹(X, Z, E, L, Y, member_in(Y, L))
U2¹(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → MEMBER_IN(Y, L)
MEMBER_IN(X, .(H, L)) → U6¹(X, H, L, member_in(X, L))
MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)
U3¹(X, Z, E, L, Y, member_out(Y, L)) → U4¹(X, Z, E, L, Y, delete_in(Y, L, V1))
U3¹(X, Z, E, L, Y, member_out(Y, L)) → DELETE_IN(Y, L, V1)
DELETE_IN(X, .(H, T1), .(H, T2)) → U8¹(X, H, T1, T2, delete_in(X, T1, T2))
DELETE_IN(X, .(H, T1), .(H, T2)) → DELETE_IN(X, T1, T2)
U4¹(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5¹(X, Z, E, L, reach_in(Y, Z, E, V1))
U4¹(X, Z, E, L, Y, delete_out(Y, L, V1)) → REACH_IN(Y, Z, E, V1)
REACH_IN(X, Y, E, L) → U1¹(X, Y, E, L, member_in(.(X, .(Y, [])), E))
REACH_IN(X, Y, E, L) → MEMBER_IN(.(X, .(Y, [])), E)

The TRS R consists of the following rules:

reach_in(X, Z, E, L) → U2(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U2(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3(X, Z, E, L, Y, member_in(Y, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U3(X, Z, E, L, Y, member_out(Y, L)) → U4(X, Z, E, L, Y, delete_in(Y, L, V1))
delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5(X, Z, E, L, reach_in(Y, Z, E, V1))
reach_in(X, Y, E, L) → U1(X, Y, E, L, member_in(.(X, .(Y, [])), E))
U1(X, Y, E, L, member_out(.(X, .(Y, [])), E)) → reach_out(X, Y, E, L)
U5(X, Z, E, L, reach_out(Y, Z, E, V1)) → reach_out(X, Z, E, L)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(H, T1), .(H, T2)) → DELETE_IN(X, T1, T2)

The TRS R consists of the following rules:

reach_in(X, Z, E, L) → U2(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U2(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3(X, Z, E, L, Y, member_in(Y, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U3(X, Z, E, L, Y, member_out(Y, L)) → U4(X, Z, E, L, Y, delete_in(Y, L, V1))
delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5(X, Z, E, L, reach_in(Y, Z, E, V1))
reach_in(X, Y, E, L) → U1(X, Y, E, L, member_in(.(X, .(Y, [])), E))
U1(X, Y, E, L, member_out(.(X, .(Y, [])), E)) → reach_out(X, Y, E, L)
U5(X, Z, E, L, reach_out(Y, Z, E, V1)) → reach_out(X, Z, E, L)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(H, T1), .(H, T2)) → DELETE_IN(X, T1, T2)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
DELETE_IN(x1, x2, x3) = DELETE_IN(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

DELETE_IN(X, .(H, T1)) → DELETE_IN(X, T1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DELETE_IN(X, .(H, T1)) → DELETE_IN(X, T1)
The graph contains the following edges 1 >= 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)

The TRS R consists of the following rules:

reach_in(X, Z, E, L) → U2(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U2(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3(X, Z, E, L, Y, member_in(Y, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U3(X, Z, E, L, Y, member_out(Y, L)) → U4(X, Z, E, L, Y, delete_in(Y, L, V1))
delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5(X, Z, E, L, reach_in(Y, Z, E, V1))
reach_in(X, Y, E, L) → U1(X, Y, E, L, member_in(.(X, .(Y, [])), E))
U1(X, Y, E, L, member_out(.(X, .(Y, [])), E)) → reach_out(X, Y, E, L)
U5(X, Z, E, L, reach_out(Y, Z, E, V1)) → reach_out(X, Z, E, L)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)

From the DPs we obtained the following set of size-change graphs:

MEMBER_IN(X, .(H, L)) → MEMBER_IN(X, L)
The graph contains the following edges 1 >= 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1_IN(X, .(H, L)) → MEMBER1_IN(X, L)

The TRS R consists of the following rules:

reach_in(X, Z, E, L) → U2(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U2(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3(X, Z, E, L, Y, member_in(Y, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U3(X, Z, E, L, Y, member_out(Y, L)) → U4(X, Z, E, L, Y, delete_in(Y, L, V1))
delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5(X, Z, E, L, reach_in(Y, Z, E, V1))
reach_in(X, Y, E, L) → U1(X, Y, E, L, member_in(.(X, .(Y, [])), E))
U1(X, Y, E, L, member_out(.(X, .(Y, [])), E)) → reach_out(X, Y, E, L)
U5(X, Z, E, L, reach_out(Y, Z, E, V1)) → reach_out(X, Z, E, L)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1_IN(X, .(H, L)) → MEMBER1_IN(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
MEMBER1_IN(x1, x2) = MEMBER1_IN(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER1_IN(.(H, L)) → MEMBER1_IN(L)

From the DPs we obtained the following set of size-change graphs:

MEMBER1_IN(.(H, L)) → MEMBER1_IN(L)
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U4¹(X, Z, E, L, Y, delete_out(Y, L, V1)) → REACH_IN(Y, Z, E, V1)
U3¹(X, Z, E, L, Y, member_out(Y, L)) → U4¹(X, Z, E, L, Y, delete_in(Y, L, V1))
REACH_IN(X, Z, E, L) → U2¹(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
U2¹(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3¹(X, Z, E, L, Y, member_in(Y, L))

The TRS R consists of the following rules:

reach_in(X, Z, E, L) → U2(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U2(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3(X, Z, E, L, Y, member_in(Y, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))
U3(X, Z, E, L, Y, member_out(Y, L)) → U4(X, Z, E, L, Y, delete_in(Y, L, V1))
delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U4(X, Z, E, L, Y, delete_out(Y, L, V1)) → U5(X, Z, E, L, reach_in(Y, Z, E, V1))
reach_in(X, Y, E, L) → U1(X, Y, E, L, member_in(.(X, .(Y, [])), E))
U1(X, Y, E, L, member_out(.(X, .(Y, [])), E)) → reach_out(X, Y, E, L)
U5(X, Z, E, L, reach_out(Y, Z, E, V1)) → reach_out(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in(x1, x2, x3, x4) = reach_in(x1, x2, x3, x4)
U2(x1, x2, x3, x4, x5) = U2(x2, x3, x4, x5)
member1_in(x1, x2) = member1_in(x2)
.(x1, x2) = .(x1, x2)
[] = []
U7(x1, x2, x3, x4) = U7(x4)
member1_out(x1, x2) = member1_out(x1)
U3(x1, x2, x3, x4, x5, x6) = U3(x2, x3, x4, x5, x6)
member_in(x1, x2) = member_in(x1, x2)
U6(x1, x2, x3, x4) = U6(x4)
member_out(x1, x2) = member_out
U4(x1, x2, x3, x4, x5, x6) = U4(x2, x3, x5, x6)
delete_in(x1, x2, x3) = delete_in(x1, x2)
U8(x1, x2, x3, x4, x5) = U8(x2, x5)
delete_out(x1, x2, x3) = delete_out(x3)
U5(x1, x2, x3, x4, x5) = U5(x5)
U1(x1, x2, x3, x4, x5) = U1(x5)
reach_out(x1, x2, x3, x4) = reach_out
REACH_IN(x1, x2, x3, x4) = REACH_IN(x1, x2, x3, x4)
U4¹(x1, x2, x3, x4, x5, x6) = U4¹(x2, x3, x5, x6)
U2¹(x1, x2, x3, x4, x5) = U2¹(x2, x3, x4, x5)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x2, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U4¹(X, Z, E, L, Y, delete_out(Y, L, V1)) → REACH_IN(Y, Z, E, V1)
U3¹(X, Z, E, L, Y, member_out(Y, L)) → U4¹(X, Z, E, L, Y, delete_in(Y, L, V1))
REACH_IN(X, Z, E, L) → U2¹(X, Z, E, L, member1_in(.(X, .(Y, [])), E))
U2¹(X, Z, E, L, member1_out(.(X, .(Y, [])), E)) → U3¹(X, Z, E, L, Y, member_in(Y, L))

The TRS R consists of the following rules:

delete_in(X, .(H, T1), .(H, T2)) → U8(X, H, T1, T2, delete_in(X, T1, T2))
delete_in(X, .(X, Y), Y) → delete_out(X, .(X, Y), Y)
member1_in(X, .(H, L)) → U7(X, H, L, member1_in(X, L))
member1_in(H, .(H, L)) → member1_out(H, .(H, L))
member_in(X, .(H, L)) → U6(X, H, L, member_in(X, L))
member_in(H, .(H, L)) → member_out(H, .(H, L))
U8(X, H, T1, T2, delete_out(X, T1, T2)) → delete_out(X, .(H, T1), .(H, T2))
U7(X, H, L, member1_out(X, L)) → member1_out(X, .(H, L))
U6(X, H, L, member_out(X, L)) → member_out(X, .(H, L))

The argument filtering Pi contains the following mapping:
member1_in(x1, x2) = member1_in(x2)
.(x1, x2) = .(x1, x2)
[] = []
U7(x1, x2, x3, x4) = U7(x4)
member1_out(x1, x2) = member1_out(x1)
member_in(x1, x2) = member_in(x1, x2)
U6(x1, x2, x3, x4) = U6(x4)
member_out(x1, x2) = member_out
delete_in(x1, x2, x3) = delete_in(x1, x2)
U8(x1, x2, x3, x4, x5) = U8(x2, x5)
delete_out(x1, x2, x3) = delete_out(x3)
REACH_IN(x1, x2, x3, x4) = REACH_IN(x1, x2, x3, x4)
U4¹(x1, x2, x3, x4, x5, x6) = U4¹(x2, x3, x5, x6)
U2¹(x1, x2, x3, x4, x5) = U2¹(x2, x3, x4, x5)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x2, x3, x4, x5, x6)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U4¹(Z, E, Y, delete_out(V1)) → REACH_IN(Y, Z, E, V1)
U3¹(Z, E, L, Y, member_out) → U4¹(Z, E, Y, delete_in(Y, L))
U2¹(Z, E, L, member1_out(.(X, .(Y, [])))) → U3¹(Z, E, L, Y, member_in(Y, L))
REACH_IN(X, Z, E, L) → U2¹(Z, E, L, member1_in(E))

The TRS R consists of the following rules:

delete_in(X, .(H, T1)) → U8(H, delete_in(X, T1))
delete_in(X, .(X, Y)) → delete_out(Y)
member1_in(.(H, L)) → U7(member1_in(L))
member1_in(.(H, L)) → member1_out(H)
member_in(X, .(H, L)) → U6(member_in(X, L))
member_in(H, .(H, L)) → member_out
U8(H, delete_out(T2)) → delete_out(.(H, T2))
U7(member1_out(X)) → member1_out(X)
U6(member_out) → member_out

The set Q consists of the following terms:

delete_in(x0, x1)
member1_in(x0)
member_in(x0, x1)
U8(x0, x1)
U7(x0)
U6(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U4¹(Z, E, Y, delete_out(V1)) → REACH_IN(Y, Z, E, V1)

The remaining pairs can at least be oriented weakly.

U3¹(Z, E, L, Y, member_out) → U4¹(Z, E, Y, delete_in(Y, L))
U2¹(Z, E, L, member1_out(.(X, .(Y, [])))) → U3¹(Z, E, L, Y, member_in(Y, L))
REACH_IN(X, Z, E, L) → U2¹(Z, E, L, member1_in(E))

Used ordering: Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₂
POL(REACH_IN(x₁, x₂, x₃, x₄)) = x₄
POL(U2¹(x₁, x₂, x₃, x₄)) = x₃
POL(U3¹(x₁, x₂, x₃, x₄, x₅)) = x₃
POL(U4¹(x₁, x₂, x₃, x₄)) = x₄
POL(U6(x₁)) = 0
POL(U7(x₁)) = 0
POL(U8(x₁, x₂)) = 1 + x₂
POL([]) = 0
POL(delete_in(x₁, x₂)) = x₂
POL(delete_out(x₁)) = 1 + x₁
POL(member1_in(x₁)) = 0
POL(member1_out(x₁)) = 0
POL(member_in(x₁, x₂)) = 0
POL(member_out) = 0

The following usable rules [17] were oriented:

delete_in(X, .(X, Y)) → delete_out(Y)
delete_in(X, .(H, T1)) → U8(H, delete_in(X, T1))
U8(H, delete_out(T2)) → delete_out(.(H, T2))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U3¹(Z, E, L, Y, member_out) → U4¹(Z, E, Y, delete_in(Y, L))
U2¹(Z, E, L, member1_out(.(X, .(Y, [])))) → U3¹(Z, E, L, Y, member_in(Y, L))
REACH_IN(X, Z, E, L) → U2¹(Z, E, L, member1_in(E))

The TRS R consists of the following rules:

delete_in(X, .(H, T1)) → U8(H, delete_in(X, T1))
delete_in(X, .(X, Y)) → delete_out(Y)
member1_in(.(H, L)) → U7(member1_in(L))
member1_in(.(H, L)) → member1_out(H)
member_in(X, .(H, L)) → U6(member_in(X, L))
member_in(H, .(H, L)) → member_out
U8(H, delete_out(T2)) → delete_out(.(H, T2))
U7(member1_out(X)) → member1_out(X)
U6(member_out) → member_out

The set Q consists of the following terms:

delete_in(x0, x1)
member1_in(x0)
member_in(x0, x1)
U8(x0, x1)
U7(x0)
U6(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 3 less nodes.